COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Facts about reverse:
C00004 00003	A proof of Ramsey's Theorem
C00005 00004	The pigeon hole principle and proofs that permutations are a group
C00010 00005	A problem in non monotonic reasoning
C00011 00006	The quantifier `there exists exactly one'
C00012 ENDMK
C⊗;
;Facts about reverse:

;File names:

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;lispax[ekl,sys]                ;axioms of LISP

;reverse[ekl,sys]               ;facts about reverse

;lthrev[ekl,sys]                ;facts about length and reverse

;Facts about reverse are given in the following order

;                lispax
;                   |    
;                   ↓                 
;                reverse           natnum
;                   |                 |
;                   |_________________|
;                            |                                       
;                            ↓
;                          lthrev
;A proof of Ramsey's Theorem

;File names:

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;natset[ekl,sys]                ;facts of set theory

;ramsey[ekl,sys]                ;proof of the theorem

;File organization:

;               natnum    
;                  ↓
;               natset
;                  ↓
;               ramsey
;The pigeon hole principle and proofs that permutations are a group
;(see the paper G.Bellin and J.Ketonen, Experiments in Authomatic Theorem Proving)
;which explains the material.

;File names:

;normal[ekl,sys]                ;a normalizer of (propositional) expressions

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;minus[ekl,sys]                 ;facts of natural numbers, involving ≤ and -

;lispax[ekl,sys]                ;axioms of LISP

;set[ekl,sys]                   ;rudiments of set theory

;length[ekl,sys]                ;length of lists

;nth[ekl,sys]                   ;the nth function and its relatives

;appl[ekl,sys]                  ;two notions of application, via lists of numbers

;sums[ekl,sys]                  ;finite sums and unions

;mult[ekl,sys]    ***bug***     ;multiplicity and their properties

;pigeon[ekl,sys]                ;the prigeon hole principle in 2nd order arithmetic

;alpig[ekl,sys]                 ;application of the pigeon hole to alists

;invima[ekl,sys]                ;a generalization (third application)

;assoc[ekl,sys]                 ;permutations are a group (using alists)

;lpig[ekl,sys]                  ;application of the pigeon hole to lists of numbers

;permp[ekl,sys]                 ;permutations are a group (lists, using predicates)

;permf[ekl,sys]                 ;permutations are a group (lists, using functions)

;File organization:

;      natnum        normal              lispax
;         |            |                    ↓
;         |____________|                   allp
;               ↓                           ↓
;             minus                        set 
;               |___________________________|
;                            ↓
;                          length
;                            ↓
;                           nth 
;                            ↓
;                           appl
;               _____________|______________________
;               ↓            ↓         ↓           ↓
;	       sums        assoc     permp        permf
;               ↓
;              mult
;               ↓
;             pigeon
;         _____________
;         ↓           ↓ 
;       alpig       lpig
;         ↓
;      invima 
 
;A problem in non monotonic reasoning

;bird[ekl,sys]                  ;most birds can fly, but not all: 
;                               ;use of the predicate `ab' (abnormal)  
;The quantifier `there exists exactly one'

;unique[ekl,sys]                ;∃!